\begin{tabbing}
$\forall$$T$:Type, ${\it ll}$:($T$ List List).
\\[0ex]($\neg$(concat(${\it ll}$) = [] $\in$ ($T$ List)))
\\[0ex]$\Rightarrow$ ($\exists$\=${\it ll}_{1}$:$T$ List List\+
\\[0ex]$\exists$\=$l_{1}$:$T$ List\+
\\[0ex](concat(${\it ll}$) = (concat(${\it ll}_{1}$) @ $l_{1}$ @ [last(concat(${\it ll}$))]) $\in$ ($T$ List)
\\[0ex]\& ${\it ll}_{1}$ @ [($l_{1}$ @ [last(concat(${\it ll}$))])] $\leq$ ${\it ll}$))
\-\-
\end{tabbing}